package inference;

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

import models.Position;
import models.formulas.DependencyFormula;
import models.formulas.Formula;
import models.terms.Dependency;
import models.terms.RDLTerm;
import models.terms.meta.MatchConstraint;
import utils.Permutation;

public class DependencyAxiom extends InferenceRule{

	int targetAssumptionIndex = 0;
	
	public DependencyAxiom(String name) {
		super(name);
	}
	
	@Override
	public Set<Formula> derive(List<Formula> assumptions, Set<RDLTerm> existTerms) {
		if (missingVariables.size() == 0) {
			return recursionDerive(assumptions, MatchConstraint.createDefault());
		} else {
			Set<Formula> result = new HashSet<>();
			for (List<RDLTerm> terms: Permutation.permutation(existTerms, missingVariables.size())) {
				for (MatchConstraint constraint: missingVariableFill(terms)) {
					if (defaultOrderConstraint != null && (! defaultOrderConstraint.check(constraint.getOrderConstraint()))) continue;
					result.addAll(recursionDerive(assumptions, constraint));
				}
			}
			return result;
		}
	}
	
	public Set<Formula> recursionDerive(List<Formula> assumptions, MatchConstraint constraint) {
		Set<Formula> result = new HashSet<>();
		Deque<Position> q = new ArrayDeque<>();
		q.add(new Position());
		Dependency baseTerm = ((DependencyFormula) assumptions.get(targetAssumptionIndex)).getDependency();
		while (! q.isEmpty()) {
			Position curPos = q.pollFirst();
			RDLTerm curTerm = baseTerm;
			for (int i = 1; i < curPos.getPath(i); i++) {
				curTerm = (RDLTerm) curTerm.getChild(curPos.getPath(i));
			}
			if (curTerm instanceof Dependency d) {
				List<Formula> assumptionsCopy = new ArrayList<Formula>(assumptions);
				assumptionsCopy.set(targetAssumptionIndex, new DependencyFormula(d));
				for (Formula derived:  super.derive(assumptionsCopy, constraint.clone())) {
					if (derived instanceof DependencyFormula df) {
						result.add(new DependencyFormula(baseTerm.replace(curPos, df.getDependency())));
					}
				}
			}
			for (int i = 0; i < curTerm.getChildren().size(); i++) {
				q.add(curPos.addPath(i));
			}
		}
		return result;
	}
	
}