package inference;

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

import exceptions.SubstituteFailedException;
import lombok.Getter;
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.MatchConstraint;
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;
		}
		
		Set<MatchConstraint> matchResult = this.conclusion.isMatchedBy(conclusion);
		Set<Formula> givenAssumptions = new HashSet<>(assumptions);
		
		for (MetaFormula assumption : this.assumptions) {
			boolean flg = false;
			for (Formula given : givenAssumptions) {
				matchResult = assumption.isMatchedBy(given, matchResult);
				if (! matchResult.isEmpty()) {
					flg = true;
					givenAssumptions.remove(given);
					break;
				}
			}
			if (!flg) {
				return false;
			}
		}
		
		if (this.defaultOrderConstraint != null) {
			for (MatchConstraint constraint: matchResult) {
				if (defaultOrderConstraint.check(constraint.getOrderConstraint())) {
					return true;
				}
			}
			return false;
		}
		
		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) {
		Set<MatchConstraint> matchResult = this.assumptions.get(0).isMatchedBy(assumptions.get(0));
		for (int i = 1; i < assumptions.size(); i++) {
			matchResult = this.assumptions.get(i).isMatchedBy(assumptions.get(i), matchResult);
			if (matchResult.isEmpty()) {
				return false;
			}
		}
		
		if (this.conclusion.isMatchedBy(conclusion, matchResult).isEmpty()) {
			return false;
		}
		if (this.defaultOrderConstraint != null) {
			for (MatchConstraint constraint: matchResult) {
				if (defaultOrderConstraint.check(constraint.getOrderConstraint())) {
					return true;
				}
			}
			return false;
		}
		return true;
	}
	
	
	public Formula apply(List<Formula> assumptions) {
		if (assumptions.size() != getAssumptionSize()) {
			return null;
		}
		Set<MatchConstraint> result = this.assumptions.get(0).isMatchedBy(assumptions.get(0));
		for (int i = 0; i < getAssumptionSize(); i++) {
			result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result);
			if (result.isEmpty()) {
				return null;
			}
		}
		return conclusion.substitution(result.iterator().next().getBinding());
	}
	
	public Set<Formula> apply(List<Formula> assumptions, Set<RDLTerm> existTerms) {
		Set<Formula> result = new HashSet<>();
		if (assumptions.size() != getAssumptionSize()) {
			return null;
		}
		Set<MatchConstraint> res = this.assumptions.get(0).isMatchedBy(assumptions.get(0));
		for (int i = 0; i < getAssumptionSize(); i++) {
			res = this.assumptions.get(i).isMatchedBy(assumptions.get(i), res); 
			if (res.isEmpty()) {
				return result;
			}
		}
		for (MatchConstraint constraint : res) {
			try {
				result.add(conclusion.substitution(constraint.getBinding()));
			} catch (SubstituteFailedException e) {}
		}
		for (RDLTerm term : existTerms) {
			Set<MatchConstraint> localConstraints = new HashSet<>(res.stream().map(v -> new MatchConstraint(v)).toList());
			if (conclusion instanceof MetaEquationFormula equation) {
				localConstraints= equation.getLeftSideHand().isMatchedBy(term, localConstraints);
			}
			else if (conclusion instanceof MetaDependencyFormula dependency) {
				localConstraints = dependency.getDependency().isMatchedBy(term, localConstraints);
			} 
			for (MatchConstraint constraint : localConstraints) {
				result.add(conclusion.substitution(constraint.getBinding()));
			}
		}
		for (RDLTerm term : existTerms) {
			Set<MatchConstraint> localConstraints = new HashSet<>(res.stream().map(v -> new MatchConstraint(v)).toList());
			if (conclusion instanceof MetaEquationFormula equation) {
				localConstraints= equation.getRightSideHand().isMatchedBy(term, localConstraints);
			}
			for (MatchConstraint constraint : localConstraints) {
				result.add(conclusion.substitution(constraint.getBinding()));
			}
		}
		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++) {
				Set<MatchConstraint> result =  this.assumptions.get(i).isMatchedBy(assumptionList.get(i));
				if (result.isEmpty()) {
					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();
	}
	
}