package inference;

import java.util.ArrayList;
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.MetaFormula;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaVariable;

public class InferenceRule {

	@Getter
	protected String name;
	
	@Getter
	protected List<MetaFormula> assumptions = new ArrayList<>();
	@Getter
	protected MetaFormula conclusion;
	protected InferenceOrderConstraint defaultOrderConstraint;
	
	protected List<MetaVariable> missingVariables;
	
	protected InferenceRule(String name) {
		this.name = name;
	}
	
	public InferenceRule(String name, List<MetaFormula> assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) {
		this.name = name;
		this.assumptions = assumptions;
		this.conclusion = conclusion;
		this.defaultOrderConstraint = constraint;
		Set<MetaVariable> missingVariables = conclusion.getAllVariables();
		for (MetaFormula assumption: assumptions) {
			missingVariables.removeAll(assumption.getAllVariables());
		}
		this.missingVariables = new ArrayList<>(missingVariables);
	}
	
	public InferenceRule(String name, List<MetaFormula> assumptions, MetaFormula conclusion) {
		this(name, assumptions, conclusion, null);
	}
	
	public Set<Formula> derive(List<Formula> assumptions) {
		return derive(assumptions, MatchConstraint.createDefault());
	}
	
	public Set<Formula> derive(List<Formula> assumptions, MatchConstraint constraint) {
		Set<Formula> result = new HashSet<>();
		if (this.assumptions.size() != assumptions.size()) {
			return new HashSet<>();
		}
		Set<MatchConstraint> matchResult = assumptionMatch(assumptions, constraint);
		
		for (MatchConstraint res: matchResult) {
			try {
				result.add(this.conclusion.substitution(res.getBinding(), res.getContext()));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return result;
	}
	
	protected Set<MatchConstraint> assumptionMatch(List<Formula>assumptions, MatchConstraint constraint) {
		Set<MatchConstraint> matchResult = new HashSet<>();
		matchResult.add(constraint);
		for (int i = 0; i < assumptions.size(); i++) {
			Formula assumption = assumptions.get(i);
			MetaFormula metaAssumption = this.assumptions.get(i);
			matchResult = metaAssumption.isMatchedBy(assumption, matchResult);
			if (matchResult.isEmpty()) {
				return new HashSet<>();
			}
		}
		return matchResult;
	}
	
//	public Set<Formula> apply(Set<Formula> formulas, Set<RDLTerm> existTerms) {
//		List<List<Formula>> matchFormulas = new ArrayList<>();
//		List<List<RDLTerm>> matchTerms = new ArrayList<>();
//		Set<Formula> result = new HashSet<>();
//		for (int i = 0; i < assumptions.size(); i++) {
//			matchFormulas.add(new ArrayList<>());
//			for (Formula formula: formulas) {
//				if (! assumptions.get(i).isMatchedBy(formula).isEmpty()) {
//					matchFormulas.get(i).add(formula);
//				}
//			}
//			if (matchFormulas.get(i).isEmpty()) { 
//				return new HashSet<>();
//			}
//		}
//		for (int i = 0; i < missingVariables.size(); i++) {
//			matchTerms.add(new ArrayList<>());
//			for (RDLTerm term : existTerms) {
//				if (! missingVariables.get(i).isMatchedBy(term).isEmpty()) {
//					matchTerms.get(i).add(term);
//				}
//			}
//			if (matchTerms.get(i).isEmpty()) {
//				return new HashSet<>();
//			}
//		}
//		if (matchFormulas.size() == 0) {
//			for (List<RDLTerm> terms : Product.product(matchTerms)) {
//				MatchConstraint constraint = MatchConstraint.createDefault();
//				for (int i = 0; i < terms.size(); i++) {
//					MetaVariable variable = missingVariables.get(i);
//					RDLTerm term = terms.get(i);
//					constraint.setBinding(variable.getVariableName(), term);
//					Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
//					if (conclusionCheck(conclusion, constraint, formulas)) {
//						result.add(conclusion);
//					}
//				}
//			}
//		}
//		for (List<Formula> assumptions: Product.product(matchFormulas)) {
//			Set<MatchConstraint> matchResult = matchCheck(assumptions);
//			if (matchResult.isEmpty()) {
//				continue;
//			}
//			for (MatchConstraint constraint: matchResult) {
//				if (missingVariables.size() == 0) {
//					try {
//						Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
//						if (conclusionCheck(conclusion, constraint, formulas)) {
//							result.add(conclusion);
//						}
//					} catch (SubstituteFailedException e) {
//						continue;
//					}
//				}
//				for (List<RDLTerm> terms : Product.product(matchTerms)) {
//					for (int i = 0; i < terms.size(); i++) {
//						MetaVariable variable = missingVariables.get(i);
//						RDLTerm term = terms.get(i);
//						constraint.setBinding(variable.getVariableName(), term);
//						try {
//							Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
//							if (conclusionCheck(conclusion, constraint, formulas)) {
//								result.add(conclusion);
//							}
//						} catch (SubstituteFailedException e) {
//							continue;
//						}
//						
//					}
//				}
//			}
//		}
//		return result;
//	}
//	
//	protected Set<MatchConstraint> matchCheck(List<Formula> assumptions) {
//		Set<MatchConstraint> matchResult = new HashSet<>();
//		matchResult.add(MatchConstraint.createDefault());
//		for (int i = 0; i < assumptions.size(); i++) {
//			Formula assumption = assumptions.get(i);
//			MetaFormula metaAssumption = this.assumptions.get(i);
//			matchResult = metaAssumption.isMatchedBy(assumption, matchResult);
//			if (matchResult.isEmpty()) {
//				return new HashSet<>();
//			}
//		}
//		return matchResult;
//	}
	
	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();
	}
	
}