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.Expression;
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.MetaDependency;
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;
import utils.ExpressionUtils;

public class RightNormalization extends EquationAxiom {

	private final Expression n1 = ExpressionUtils.parse("n-1");
	
	public RightNormalization() {
		super("RIght Normalization");
		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), n1);
									}
								},
								new MetaDependency(
										new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
										new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"))
								)
						)
				)
		);
		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("secondAssumptionIndex", curIndex + 1);
										return new MetaEvaluatableTermVariable(new Variable("w" + curIndex), n1);
									}
								},
								new MetaEvaluatableTermVariable(new Variable("u"), n1)
						)
				)
		);
		
		assumptions.add(
				new MetaEquationFormula(
						new MetaDependencyTerm(
								new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
								new MetaEvaluatableTermVariable(new Variable("xxx")),
								new MetaEvaluatableTermVariable(new Variable("yyy"))
						),
						new MetaEvaluatableTermVariable(new Variable("u"), n1)
				)
		);
		
		conclusion = new MetaEquationFormula(
				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 + secondAssumptionIndex) * 2) {
									return null;
								}
								if (curIndex < firstAssumptionIndex * 2) {
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2), n1);
									}
									return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
								}
								curIndex -= firstAssumptionIndex * 2;
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("w" + curIndex / 2), n1);
								}
								return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2));
							}
						},
						new MetaDependencyTerm(
								new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
								new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
								new MetaEvaluatableTermVariable(new Variable("u"), n1)
						)
				),
				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), n1);
								}
								return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
							}
							
						},
						new MetaDependencyTerm(
								new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
								new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
								new MetaDynamicDependencyTerm(
										new MetaTermGenerator() {
											@Override
											public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
												curIndex -= 1;
												int secondAssumptionIndex = (Integer) context.get("secondAssumptionIndex");
												if (curIndex >= secondAssumptionIndex * 2) {
													return null;
												}
												if (curIndex % 2 == 0) {
													return new MetaEvaluatableTermVariable(new Variable("w" + curIndex / 2), n1);
												}
												return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2));
											}
											
										},
										new MetaEvaluatableTermVariable(new Variable("u"), n1)
								)
						)
				)
		);
		
	}

	@Override
	protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
		if (assumptions.size() < 3) {
			return new HashSet<>();
		}
		Set<MatchConstraint> result = new HashSet<>();
		result.add(constraint);
		Map<String, Object> context = new HashMap<>();
		for (int i = 0; i < 3; i++) {
			result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result);
			if (result.isEmpty()) {
				return new HashSet<>();
			}
		}
		
		int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex");
		int secondAssumptionIndex = (Integer) context.get("secondAssumptionIndex");
		if (assumptions.size() < 3 + firstAssumptionIndex + secondAssumptionIndex) {
			return new HashSet<>();
		}
		for (int i = 0; i < firstAssumptionIndex; i++) {
			Formula assumption = assumptions.get(i + 3);
			MetaEquationFormula mef = new MetaEquationFormula(
					new MetaDependencyTerm(
							new MetaEvaluatableTermVariable(new Variable("v" + i), n1),
							new MetaEvaluatableTermVariable(new Variable("xxxx" + i)),
							new MetaEvaluatableTermVariable(new Variable("yyyy" + i))
					),
					new MetaEvaluatableTermVariable(new Variable("x" + i))
			);
			result = mef.isMatchedBy(assumption, result);
			if (result.isEmpty()) {
				return new HashSet<>();
			}
		}
		
		for(int i = 0; i < secondAssumptionIndex; i++) {
			Formula assumption = assumptions.get(i + 3 + firstAssumptionIndex);
			MetaEquationFormula mef = new MetaEquationFormula(
					new MetaDependencyTerm(
							new MetaEvaluatableTermVariable(new Variable("w" + i), n1),
							new MetaEvaluatableTermVariable(new Variable("xxyy" + i)),
							new MetaEvaluatableTermVariable(new Variable("yyxx" + i))
					),
					new MetaEvaluatableTermVariable(new Variable("y" + i))
			);
			result = mef.isMatchedBy(assumption, result);
			if (result.isEmpty()) {
				return new HashSet<>();
			}
		}
		
		Set<Formula> subRes = new HashSet<>();
		for (MatchConstraint con: result) {
			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;
	}
	
	
	
}