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.Constant;
import models.algebra.Variable;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.DependencyTerm;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDependencyTerm;
import models.terms.meta.MetaDynamicDependencyTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;

public class Constantness extends EquationAxiom {

	public Constantness() {
		super("Constantness");
	}

	@Override
	protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
		Set<MatchConstraint> result = new HashSet<>();
		Map<String, Object> context = new HashMap<>();
		result.add(constraint);
		int prevOrder = 0;
		int m = 0;
		int n = 1;
		if (assumptions.get(0) instanceof EquationFormula eq) {
			if (eq.getLeftSideHand() instanceof DependencyTerm dt) {
				prevOrder = dt.getDependingTerm().getOrder();
				m = prevOrder;
			} else {
				return new HashSet<>();
			}
		} else {
			return new HashSet<>();
		}
		
		for (int i = 1; i < assumptions.size(); i++) {
			if (assumptions.get(i) instanceof EquationFormula eq2) {
				if (eq2.getLeftSideHand() instanceof DependencyTerm dt) {
					int order = dt.getDependingTerm().getOrder();
					n = order;
					if (prevOrder - order != 1) {
						return new HashSet<>();
					}
					prevOrder = order;
				} else {
					return new HashSet<>();
				}
			} else {
				return new HashSet<>();
			}
		}
		
		if (n >= m) {
			return new HashSet<>();
		}
		
		if (m - n != assumptions.size()) {
			return new HashSet<>();
		}
		
		for (int i = 0; i < assumptions.size(); i++) {
			Formula assumption = assumptions.get(i);
			MetaDependencyTerm mdt = new MetaDependencyTerm(
					new MetaEvaluatableTermVariable(new Variable("r" + i), new Constant("" + (m + i))),
					new MetaEvaluatableTermVariable(new Variable("xxx" + i)),
					new MetaEvaluatableTermVariable(new Variable("yyy" + i))
			);
			MetaEquationFormula mef = new MetaEquationFormula(mdt, new MetaEvaluatableTermVariable(new Variable("t" + i)));
			result = mef.isMatchedBy(assumption, result);
			if (result.isEmpty()) {
				return new HashSet<>();
			}
		}
		
		MetaEquationFormula conclusion = new MetaEquationFormula(
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								int n = (Integer) context.get("n");
								int m = (Integer) context.get("m");
								int i = maxDepth - curDepth - 1;
								if (curDepth == maxDepth - 1) {
									return new MetaDependencyTerm(
											new MetaEvaluatableTermVariable(new Variable("se"), new Constant("" + n)),
											new MetaEvaluatableTermVariable(new Variable("r" + i), new Constant("" + (m + i))),
											new MetaEvaluatableTermVariable(new Variable("t" + i))
									);
								}
								if (curIndex == 0) {
									return new MetaDynamicDependencyTerm(this);
								} else if (curIndex == 1) {
									return new MetaEvaluatableTermVariable(new Variable("r" + i), new Constant("" + (m + i)));
								} 
								return new MetaEvaluatableTermVariable(new Variable("t" + i));
							}
						}
				),
				new MetaEvaluatableTermVariable(new Variable("se"), new Constant("" + n))
		);
		
		Set<Formula> subRes = new HashSet<>();
		for (MatchConstraint con: result) {
			try {
				int maxIndex = 3;
				int maxDepth = m - n;
				context.put("maxIndex", maxIndex);
				context.put("maxDepth", maxDepth);
				context.put("n", n);
				context.put("m", m);
				subRes.add(conclusion.substitution(con.getBinding(), context));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		
		return super.apply(assumptions, constraint);
	}

	
	
	
}