package inference;
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Deque;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import exceptions.SubstituteFailedException;
import models.Position;
import models.formulas.DependencyFormula;
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);
	}
	
	protected EquationAxiom(String name) {
		super(name);
	}
	
	public Set<EvaluatableTerm> apply(List<Formula> assumptions, EvaluatableTerm term) {
		return apply(assumptions, term, MatchConstraint.createDefault());
	}
	
	public Set<EvaluatableTerm> apply(List<Formula>assumptions,  EvaluatableTerm term, MatchConstraint constraint) {
		Set<EvaluatableTerm> result = new HashSet<>();
		if (assumptions.size() < this.assumptions.size()) {
			return new HashSet<>();
		}
		
		Set<MatchConstraint> matchResult = assumptionMatch(assumptions, constraint);
		
		Set<MatchConstraint> conclusionLeftMatchResult = conclusionLeftSideHandMatch(term, matchResult);
		for (MatchConstraint leftConst: conclusionLeftMatchResult) {
			leftConst.getContext().put("isLeft", true);
		}
		Set<MatchConstraint> conclusionRightMatchResult = conclusionRightSideHandMatch(term, matchResult);
		for (MatchConstraint rightConst: conclusionRightMatchResult) {
			rightConst.getContext().put("isLeft", false);
		}
		Set<MatchConstraint> conclusionMatchResult = new HashSet<>();
		conclusionMatchResult.addAll(conclusionLeftMatchResult);
		conclusionMatchResult.addAll(conclusionRightMatchResult);
		
		MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion;
		for (MatchConstraint matchRes: conclusionMatchResult) {
			boolean isLeft =(Boolean) matchRes.getContext().get("isLeft");
			if (defaultOrderConstraint != null && ! defaultOrderConstraint.check(matchRes.getOrderConstraint())) {
				continue;
			}
			try {
				if (isLeft) {
					result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightSideHand()).substitute(matchRes.getBinding(), matchRes.getContext()));
				} else {
					result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftSideHand()).substitute(matchRes.getBinding(), matchRes.getContext()));
				}
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return result;
	}
	
	
	protected Set<MatchConstraint> conclusionLeftSideHandMatch(EvaluatableTerm term, Set<MatchConstraint> matchResult) {
		MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion;
		return ((MetaRDLTerm) metaConclusion.getLeftSideHand()).isMatchedBy(term, matchResult);
	}
	
	protected Set<MatchConstraint> conclusionRightSideHandMatch(EvaluatableTerm term, Set<MatchConstraint> matchResult) {
		MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion;
		return ((MetaRDLTerm) metaConclusion.getRightSideHand()).isMatchedBy(term, matchResult);
	}
	
	
	protected 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;
	}
	
	protected static boolean conclusionCheck(EvaluatableTerm leftSideHand, Set<Formula> formulas) {
		for (Formula formula: requiredAssumptions(leftSideHand)) {
			if (! formulas.contains(formula)) { 
				return false;
			}
		}
		return true;
	}
	
	protected static Map<MatchConstraint, Map<Position, Integer>> savePositions(Set<MatchConstraint> matchConstraint) {
		Map<MatchConstraint, Map<Position, Integer>> result = new HashMap<>();
		for (MatchConstraint constraint : matchConstraint) {
			Deque<Position> posDeque = new ArrayDeque<>();
			posDeque.add(new Position());
			Map<Position, Integer> posMap = new HashMap<>();
			while (posDeque.size() != 0) {
				Position pos = posDeque.pollFirst();
				if (! constraint.getContext().containsKey(pos)) {
					continue;
				}
				int i = 0;
				while (true) {
					Position nextPos = pos.addPath(i);
					if (! constraint.getContext().containsKey(nextPos)) {
						break;
					}
					posMap.put(pos, (Integer) constraint.getContext().get(pos));
					posDeque.add(nextPos);
				}
			}
			result.put(constraint, posMap);
		}
		return result;
	}
	
}