package inference;

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 exceptions.SubstituteFailedException;
import lombok.Getter;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.formulas.meta.MetaFormula;
import models.terms.RDLTerm;
import models.terms.meta.OrderVariableConstraint;
import utils.Permutation;

public class InferenceRule {

	@Getter
	private final String name;
	
	@Getter
	private final List<MetaFormula> assumptions;
	@Getter
	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;
		}
		
		Map<Variable, RDLTerm> binding = new HashMap<>();
		Map<Variable, OrderVariableConstraint> orderConstraints = new HashMap<>();
		this.conclusion.isMatchedBy(conclusion, binding, orderConstraints);
		Set<Formula> givenAssumptions = new HashSet<>(assumptions);
		
		for (MetaFormula assumption : this.assumptions) {
			boolean flg = false;
			for (Formula given : givenAssumptions) {
				Map<Variable, RDLTerm> tmpBinding = new HashMap<>(binding);
				Map<Variable, OrderVariableConstraint> tmpOrderConstraints = new HashMap<>(orderConstraints);
				if (assumption.isMatchedBy(given, tmpBinding, tmpOrderConstraints)) {
					binding.putAll(tmpBinding);
					orderConstraints.putAll(tmpOrderConstraints);
					flg = true;
					givenAssumptions.remove(given);
					break;
				}
			}
			if (!flg) {
				return false;
			}
		}
		
		if (this.defaultOrderConstraint != null) {
			return defaultOrderConstraint.check(orderConstraints);
		}
		
		return true;
		
//		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;
	}
	
	
	public Formula apply(List<Formula> assumptions) {
		if (assumptions.size() != getAssumptionSize()) {
			return null;
		}
		Map<Variable, RDLTerm> binding = new HashMap<>();
		Map<Variable, OrderVariableConstraint> orderConstraint = new HashMap<>();
		for (int i = 0; i < getAssumptionSize(); i++) {
			if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraint)) {
				return null;
			}
		}
		return conclusion.substitution(binding);
	}
	
	public Set<Formula> apply(List<Formula> assumptions, Set<RDLTerm> existTerms) {
		Set<Formula> result = new HashSet<>();
		if (assumptions.size() != getAssumptionSize()) {
			return null;
		}
		Map<Variable, RDLTerm> binding = new HashMap<>();
		Map<Variable, OrderVariableConstraint> orderConstraint = new HashMap<>();
		for (int i = 0; i < getAssumptionSize(); i++) {
			if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraint)) {
				return result;
			}
		}
		try {
			result.add(conclusion.substitution(binding));
		} catch (SubstituteFailedException e) {
			
		}
		for (RDLTerm term : existTerms) {
			Map<Variable, RDLTerm> localBinding = new HashMap<>(binding);
			Map<Variable, OrderVariableConstraint> localOrderConstraint = new HashMap<>(orderConstraint);
			if (conclusion instanceof MetaEquationFormula) {
				MetaEquationFormula equation = (MetaEquationFormula) conclusion;
				if (equation.getLeftSideHand().isMatchedBy(term, localBinding, localOrderConstraint)) {
					result.add(conclusion.substitution(localBinding));
				}
			}
			else if (conclusion instanceof MetaDependencyFormula) {
				MetaDependencyFormula dependency = (MetaDependencyFormula) conclusion;
				if (dependency.getDependency().isMatchedBy(term, localBinding, localOrderConstraint)) {
					result.add(conclusion.substitution(localBinding));
				}
			} 
		}
		
		for (RDLTerm term : existTerms) {
			Map<Variable, RDLTerm> localBinding = new HashMap<>(binding);
			Map<Variable, OrderVariableConstraint> localOrderConstraint = new HashMap<>(orderConstraint);
			if (conclusion instanceof MetaEquationFormula) {
				MetaEquationFormula equation = (MetaEquationFormula) conclusion;
				if (equation.getRightSideHand().isMatchedBy(term, localBinding, localOrderConstraint)) {
					result.add(conclusion.substitution(localBinding));
				}
			}
		}
		return result; 
	}
	
	public Formula apply(Collection<Formula> assumptions) {
		if (assumptions.size() != getAssumptionSize()) {
			return null;
		}
		for (List<Formula> assumptionList : Permutation.permutation(assumptions, assumptions.size())) {
			boolean matchFailed = false;
			for (int i = 0; i < getAssumptionSize(); i++) {
				if (! this.assumptions.get(i).isMatchedBy(assumptionList.get(i))) {
					matchFailed = true;
					break;
				}
			}
			if (matchFailed) {
				continue;
			} else {
				return apply(assumptionList);
			}
		}
		return null;
	}
	
	
	public int getAssumptionSize() {
		return this.assumptions.size();
	}
	
	
	public String toString() {
		StringBuilder sb = new StringBuilder();
		if (defaultOrderConstraint != null) {
			sb.append(defaultOrderConstraint);
			sb.append(", ");
		}
		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())) + "  (" + this.name + ")";
		sb = new StringBuilder();
		sb.append(assumpStr);
		sb.append("\n");
		sb.append(line);
		sb.append("\n");
		sb.append(concluStr);
		return sb.toString();
	}
	
	@Override
	public boolean equals(Object another) {
		if (! (another instanceof InferenceRule)) {
			return false;
		}
		InferenceRule anotherRule = (InferenceRule) another;
		return getName().equals(anotherRule.getName());
	}
	
	@Override
	public int hashCode() {
		return getName().hashCode();
	}
	
}