package inference;

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

import lombok.Getter;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.meta.MetaEquationFormula;
import models.formulas.meta.MetaFormula;
import models.terms.DependencyTerm;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import models.terms.Resource;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaVariable;
import utils.Product;

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> 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) {
					Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
					if (conclusionCheck(conclusion, constraint, formulas)) {
						result.add(conclusion);
					}
				}
				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);
						Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
						if (conclusionCheck(conclusion, constraint, formulas)) {
							result.add(conclusion);
						}
					}
				}
			}
		}
		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;
	}
	
	private static Set<Formula> requiredAssumptions(EvaluatableTerm term) {
		if (term instanceof Resource) {
			return new HashSet<>();
		}
		DependencyTerm depTerm = (DependencyTerm) term;
		Set<Formula> result = new HashSet<>();
		EvaluatableTerm dependingTerm = depTerm.getDependingTerm();
		List<EvaluatableTerm> dependedTerms = depTerm.getDependedTerms();
		List<EvaluatableTerm> argumentTerms = depTerm.getArgumentTerms();
		for (int i = 0; i < dependedTerms.size(); i++) {
			EvaluatableTerm dependedTerm = dependedTerms.get(i);
			EvaluatableTerm argTerm = argumentTerms.get(i);
			In in = new In(argTerm, dependedTerm);
			result.add(in);
		}
		if (dependingTerm instanceof Resource) {
			result.add(new DependencyFormula(dependingTerm, dependedTerms));
		} else if (dependingTerm instanceof DependencyTerm depending) {
			for (Formula formula : requiredAssumptions(depending)) {
				if (formula instanceof DependencyFormula dependency) {
					DependencyTerm newDependingTerm = new DependencyTerm((EvaluatableTerm) dependency.getDependency().getDependingTerm(), dependedTerms, argumentTerms);
					List<EvaluatableTerm> newDependedTerms = new ArrayList<>();
					for (RDLTerm dependedTerm : dependency.getDependency().getDependedTerms()) {
						newDependedTerms.add(new DependencyTerm((EvaluatableTerm) dependedTerm, dependedTerms, argumentTerms));
					}
					result.add(new DependencyFormula(newDependingTerm, newDependedTerms));
				} else if(formula instanceof In in) {
					result.add(new In(new DependencyTerm(in.getLeftSideHand(), dependedTerms, argumentTerms), new DependencyTerm(in.getRightSideHand(), dependedTerms, argumentTerms)));
				}
			}
		}
		return result;
	}
	
	private static boolean conclusionCheck(Formula conclusion, MatchConstraint constraint, Set<Formula> formulas) {
		if (conclusion instanceof DependencyFormula) return true;
		EquationFormula eq = (EquationFormula) conclusion;
		EvaluatableTerm leftSideHand = eq.getLeftSideHand();
		for (Formula formula: requiredAssumptions(leftSideHand)) {
			if (formula instanceof DependencyFormula dep) {
				if (! formulas.contains(dep)) { 
					return false;
				}
			} else if (formula instanceof In in) {
				boolean flg = false;
				for (MetaEquationFormula metaFormula: in.deriveRule()) {
					for (Formula existFormula: formulas) {
						if (! metaFormula.isMatchedBy(existFormula, constraint).isEmpty()) {
							flg = true;
							break;
						}
					}
					if (flg) break;
				}
				if (!flg) {
					return false;
				}
			}
		}
		return true;
	}
	
	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();
	}
	
}