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

import exceptions.SubstituteFailedException;
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.MetaRDLTerm;

public class EquationAxiom extends InferenceRule {

	public EquationAxiom(String name, List<MetaFormula> assumptions, MetaEquationFormula conclusion, InferenceOrderConstraint constraint) {
		super(name, assumptions, conclusion, constraint);
	}
	
	public EquationAxiom(String name, List<MetaFormula> assumptions, MetaEquationFormula conclusion) {
		super(name, assumptions, conclusion);
	}
	
	public Set<EquationFormula> apply(List<Formula>assumptions,  EvaluatableTerm leftSideHand) {
		Set<EquationFormula> result = new HashSet<>();
		if (assumptions.size() < this.assumptions.size()) {
			return new HashSet<>();
		}
		MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion;
		Set<MatchConstraint> matchResult = ((MetaRDLTerm) metaConclusion.getLeftSideHand()).isMatchedBy(leftSideHand);
		if (result.isEmpty()) {
			return new HashSet<>();
		}
		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 (result.isEmpty()) {
				return new HashSet<>();
			}
		}
		for (MatchConstraint matchRes: matchResult) {
			try {
				result.add(metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext()));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return result;
	}
	
	
	
	private static Set<DependencyFormula> requiredAssumptions(EvaluatableTerm term) {
		if (term instanceof Resource) {
			return new HashSet<>();
		}
		DependencyTerm depTerm = (DependencyTerm) term;
		Set<DependencyFormula> result = new HashSet<>();
		EvaluatableTerm dependingTerm = depTerm.getDependingTerm();
		List<EvaluatableTerm> dependedTerms = depTerm.getDependedTerms();
		List<EvaluatableTerm> argumentTerms = depTerm.getArgumentTerms();
		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));
				} 
			}
		}
		return result;
	}
	
	private static boolean conclusionCheck(EvaluatableTerm leftSideHand, Set<Formula> formulas) {
		for (Formula formula: requiredAssumptions(leftSideHand)) {
			if (! formulas.contains(formula)) { 
				return false;
			}
		}
		return true;
	}
	
}