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 exceptions.SubstituteFailedException;
import lombok.Getter;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaFormula;
import models.terms.RDLTerm;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaVariable;
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;
		}
		
		for(List<Formula> assumption : Permutation.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 Set<Formula> apply(List<Formula> assumptions, Set<RDLTerm> existTerms) {
		Set<Formula> result = new HashSet<>();
		Set<MetaVariable> assumptionVariables = new HashSet<>();
		Set<MetaVariable> conclusionVariables = new HashSet<>();
		for (MetaFormula assumption: this.assumptions) {
			assumptionVariables.addAll(assumption.getSubTerms(MetaVariable.class));
		}
		conclusionVariables.addAll(conclusion.getSubTerms(MetaVariable.class));
		
		conclusionVariables.removeAll(assumptionVariables);
		List<MetaVariable> leftVariables = new ArrayList<>(conclusionVariables);
		
		if (! conclusionVariables.isEmpty()) {
			for (List<RDLTerm> variables: Permutation.permutation(existTerms, leftVariables.size())) {
				Map<Variable, RDLTerm> binding = new HashMap<>();
				for (int i = 0; i < variables.size(); i++) {
					binding.put(leftVariables.get(i).getVariableName(), variables.get(i));
				}
				try {
					Formula res = apply(assumptions, new MatchConstraint(binding, new HashMap<>()));
					if (res != null) {
						Set<MatchConstraint> constraints = conclusion.isMatchedBy(res);
						boolean flg = true;
						for (MatchConstraint constraint : constraints) {
							if (! defaultOrderConstraint.check(constraint.getOrderConstraint())) {
								flg = false;
								break;
							}
						} 
						if (flg) {
							result.add(res);
						}
					}
				} catch (SubstituteFailedException e) {
					continue;
				}
			}
		}	
		return result;
	}
	
	public Formula apply(Formula ...assumptions) {
		return apply(Set.of(assumptions));
	}
	
	public Formula apply(Collection<Formula> assumptions) {
		if (assumptions.size() != getAssumptionSize()) {
			return null;
		}
		for (List<Formula> assumptionList : Permutation.permutation(assumptions, assumptions.size())) {
			Formula result = apply(assumptionList);
			if (result != null) {
				return result;
			}
		}
		return null;
	}
	
	private 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 = 1; 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());
	}
	
	private Formula apply(List<Formula> assumptions, MatchConstraint constraint) {
		if (assumptions.size() != getAssumptionSize()) {
			return null;
		}
		
		Set<MatchConstraint> result = new HashSet<>();
		result.add(constraint);
		for (int i = 0; i < getAssumptionSize(); i++) {
			result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result);
			if (result.isEmpty()) {
				return null;
			}
		}
		Formula subRes = conclusion.substitution(result.iterator().next().getBinding());
		return subRes;
	}
	
	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();
	}
	
}