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

public class Constantness extends InferenceRule{

	public Constantness() {
		//todo
		super("composite mapping", List.of(), null, null);
	}
	
	
	@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 = perm.size() - m;
				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) {
					OrderVariableConstraint orderConst = new OrderVariableConstraint();
					orderConst.setConstraint(n, OrderConstraint.EQ);
					MatchConstraint seConst = MatchConstraint.createDefault();
					seConst.getOrderConstraint().put(new Variable("n"), orderConst);
					if (! se.isMatchedBy(term).isEmpty()) {
						constraint.getBinding().put(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).isMatchedBy(assumptions.get(0));
		for (int i = 1; i < assumptions.size(); i++) {
			result = generateAssumption(i).isMatchedBy(assumptions.get(i), result);
		}
		return result;
	}
	
	private MetaEquationFormula generateAssumption(int i) {
		MetaRDLTerm metaAssumptionLsh = new MetaRDLTerm(
				new MetaResource(new Variable("r" + i), new Variable("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;
		if (depth == maxRecursion) {
			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), new Variable("m-"+i)),
				new MetaEvaluatableTermVariable(new Variable("t" + i))
		);
	}
	
}