package inference;

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import lombok.Getter;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaFormula;
import models.terms.RDLTerm;
import models.terms.meta.OrderVariableConstraint;

public class InferenceRule {

	@Getter
	private final String name;
	
	private final List<MetaFormula> assumptions;
	private final MetaFormula conclusion;
	private final InferenceOrderConstraint defaultOrderConstraint;
	
	public InferenceRule(String name, List<MetaFormula> assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) {
		this.name = name;
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		this.defaultOrderConstraint = constraint;
	}
	
	public InferenceRule( List<MetaFormula> assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) {
		this.name = "undefined";
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		this.defaultOrderConstraint = constraint;
	}
	
	public InferenceRule(String name, List<MetaFormula> assumptions, MetaFormula conclusion) {
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		this.name = name;
		this.defaultOrderConstraint = null;
	}
	
	public InferenceRule(List<MetaFormula> assumptions, MetaFormula conclusion) {
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		this.name = "undefined";
		this.defaultOrderConstraint = null;
	}
	
	public boolean check(Collection<Formula> assumptions, Formula conclusion) {
		if (this.assumptions.size() > assumptions.size()) {
			return false;
		}
		for(List<Formula> assumption : permutation(assumptions, this.assumptions.size())) {
			if (check(assumption, conclusion)) {
				return true;
			}
		}
		return false;
	}
	
	private boolean check(List<Formula> assumptions, Formula conclusion) {
		Map<Variable, RDLTerm> binding = new HashMap<>();
		Map<Variable, OrderVariableConstraint> orderConstraints = new HashMap<>();
		for (int i = 0; i < assumptions.size(); i++) {
			if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraints)) {
				return false;
			}
		}
		if (! this.conclusion.isMatchedBy(conclusion, binding, orderConstraints)) {
			return false;
		}
		if (this.defaultOrderConstraint != null) {
			return defaultOrderConstraint.check(orderConstraints);
		}
		return true;
	}
	
	private <T> List<List<T>> permutation(Collection<T> list, int n) {
		List<List<T>> res = new ArrayList<>();
		permutation(list, n, new ArrayList<>(), new HashSet<>(), res);
		return res;
	}
	
	private <T> void permutation(Collection<T> all, int n, List<T> current, Set<T> used, List<List<T>> result) {
		if (current.size() == n) {
			result.add(new ArrayList<>(current));
			return;
		}
		for (T elem : all) {
			if (! used.contains(elem)) {
				current.add(elem);
				used.add(elem);
				permutation(all, n, current, used, result);
				current.remove(current.size() - 1);
				used.remove(elem);
			}
		}
	}
	
	
	public String toString() {
		StringBuilder sb = new StringBuilder();
		for (int i = 0; i < assumptions.size(); i++) {
			sb.append(assumptions.get(i).toString());
			if (i != assumptions.size() - 1) {
				sb.append(", ");
			}
		}
		String assumpStr = sb.toString();
		String concluStr = conclusion.toString();
		String line = "-".repeat(Math.max(assumpStr.length(), concluStr.length()));
		sb = new StringBuilder();
		sb.append(assumpStr);
		sb.append("\n");
		sb.append(line);
		sb.append("\n");
		sb.append(concluStr);
		return sb.toString();
	}
	
}