package inference;

import java.util.HashSet;
import java.util.List;
import java.util.Set;

import exceptions.SubstituteFailedException;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.RDLTerm;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResource;
import models.terms.meta.OrderConstraint;
import models.terms.meta.OrderVariableConstraint;
import utils.ExpressionUitls;
import utils.Permutation;

public class Constantness extends InferenceRule{

	public Constantness() {
		//todo
		super("composite mapping", List.of(), null, new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")));
	}
	
	
	@Override
	public Set<Formula> apply(List<Formula> assumptions, Set<RDLTerm> existTerms) {
		Set<Formula> result = new HashSet<>();
		for (List<Formula> perm : Permutation.permutation(assumptions, assumptions.size())) {
			Set<MatchConstraint> matchResult = assumptionMatch(perm);
			for (MatchConstraint constraint: matchResult) {
				int m = constraint.getOrderConstraint().get(new Variable("m")).getOrder();
				int n = m - perm.size();
				
				
				if (! constraint.getOrderConstraint().containsKey(new Variable("n"))) {
					constraint.putOrderConstraint(new Variable("n"), new OrderVariableConstraint());
				}
				constraint.setOrderConstraint(new Variable("n"), OrderConstraint.EQ, n);
				
				if (! this.defaultOrderConstraint.check(constraint.getOrderConstraint())) {
					continue;
				}
				
				MetaRDLTerm conclusionLsh = createMetaConclusionLsh(0, m-n);
				MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"));
				MetaEquationFormula conclusion = new MetaEquationFormula(conclusionLsh, se);
				
				for (RDLTerm term : existTerms) {
					if (! se.isMatchedBy(term).isEmpty()) {
						constraint.setBinding(new Variable("se"), term);
						try {
							result.add(conclusion.substitution(constraint.getBinding()));
						} catch(SubstituteFailedException e) {
							continue;
						}
					}
				}
			}
		}
		return result;
	}
	
	private Set<MatchConstraint> assumptionMatch(List<Formula> assumptions) {
		Set<MatchConstraint> result = new HashSet<>();
		result = generateAssumption(0, false).isMatchedBy(assumptions.get(0));
		for (int i = 1; i < assumptions.size(); i++) {
			result = generateAssumption(i, i == assumptions.size() - 1).isMatchedBy(assumptions.get(i), result);
		}
		
		return result;
	}
	
	private MetaEquationFormula generateAssumption(int i, boolean isLast) {
		if (isLast) {
			MetaRDLTerm metaAssumptionLsh = new MetaRDLTerm(
					new MetaResource(new Variable("r" + i), ExpressionUitls.parse("n + 1")),
					new MetaEvaluatableTermVariable(new Variable("x" + i)),
					new MetaEvaluatableTermVariable(new Variable("y" + i))
			);
			MetaEvaluatableTermVariable metaAssumptionRsh = new MetaEvaluatableTermVariable(new Variable("t" + i));
			return new MetaEquationFormula(metaAssumptionLsh, metaAssumptionRsh);
		} else {
			MetaRDLTerm metaAssumptionLsh = new MetaRDLTerm(
					new MetaResource(new Variable("r" + i), ExpressionUitls.parse("m - " + i)),
					new MetaEvaluatableTermVariable(new Variable("x" + i)),
					new MetaEvaluatableTermVariable(new Variable("y" + i))
			);
			MetaEvaluatableTermVariable metaAssumptionRsh = new MetaEvaluatableTermVariable(new Variable("t" + i));
			return new MetaEquationFormula(metaAssumptionLsh, metaAssumptionRsh);
		}
	}
	
	private MetaRDLTerm createMetaConclusionLsh(int depth, int maxRecursion) {
		int i = maxRecursion - depth - 1;
		if (depth == maxRecursion - 1) {
			return new MetaRDLTerm(
					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
					new MetaResource(new Variable("r" + i), new Variable("m")),
					new MetaEvaluatableTermVariable(new Variable("t" + i))
			);
		}
		return new MetaRDLTerm(
				createMetaConclusionLsh(depth + 1, maxRecursion),
				new MetaResource(new Variable("r" + i),ExpressionUitls.parse("m - " + i)),
				new MetaEvaluatableTermVariable(new Variable("t" + i))
		);
	}
	
}