package inference;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
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.MetaRDLTerm;
import models.terms.meta.MetaVariable;
import utils.Permutation;

public class InferenceRule {

	@Getter
	protected String name;
	
	@Getter
	protected List<MetaFormula> assumptions = new ArrayList<>();
	@Getter
	protected MetaFormula conclusion;
	protected InferenceOrderConstraint defaultOrderConstraint;
	
	protected List<MetaFormula> repetitionAssumptions = new ArrayList<>();
	protected ConclusionSizeCalculator conclusionMaxIndexCalculator;
	protected ConclusionSizeCalculator conclusionMaxDepthCalculator;
	protected AssumptionSizeCalculator assumptionRepetitionSizeCalculator;
	
	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;
	}
	
	public InferenceRule(
			String name,
			List<MetaFormula> assumptions, 
			List<MetaFormula> repetitionAssumptions, 
			MetaFormula conclusion, 
			InferenceOrderConstraint constraint,
			ConclusionSizeCalculator conclusionMaxIndexCalculator,
			ConclusionSizeCalculator conclusionMaxDepthCalculator,
			AssumptionSizeCalculator assumptionSizeCalculator
	) {
		this.name = name;
		this.assumptions = assumptions;
		this.repetitionAssumptions = repetitionAssumptions;
		this.conclusion = conclusion;
		this.defaultOrderConstraint = constraint;
		this.conclusionMaxIndexCalculator = conclusionMaxIndexCalculator;
		this.conclusionMaxDepthCalculator = conclusionMaxDepthCalculator;
		this.assumptionRepetitionSizeCalculator = assumptionSizeCalculator;
	}
	
	public InferenceRule( List<MetaFormula> assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) {
		this("undefined", assumptions, conclusion, constraint);
	}
	
	public InferenceRule(String name, List<MetaFormula> assumptions, MetaFormula conclusion) {
		this(name, assumptions, conclusion, null);
	}
	
	public InferenceRule(List<MetaFormula> assumptions, MetaFormula conclusion) {
		this("undefined", assumptions, conclusion, null);
	}
	
	
	public Set<Formula> apply(Formula ...assumptions) {
		return apply(Set.of(assumptions));
	}
	
	public Set<Formula> apply(Set<Formula> assumptions) {
		if (assumptions.size() < getAssumptionSize()) {
			return new HashSet<>();
		}
		Set<Formula> result = new HashSet<>();
		for (List<Formula> assumptionList : Permutation.permutation(assumptions, assumptions.size())) {
			result.addAll(apply(assumptionList));
		}
		return result;
	}
	
	protected Set<Formula> apply(List<Formula> assumptions) {
		return apply(assumptions, MatchConstraint.createDefault());
	}
	
	protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
		Map<String, Object> context = new HashMap<>();
		if (assumptions.size() < getAssumptionSize()) {
			return new HashSet<>();
		}
		
		Set<MatchConstraint> result = new HashSet<>();
		result.add(constraint);
		for (int i = 0; i < getAssumptionSize(); i++) {
			result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result, context);
			if (result.isEmpty()) {
				return new HashSet<>();
			}
		}
		if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) {
			return new HashSet<>();
		}
		if (this.repetitionAssumptions.size() != 0) {
			for (int i = 0; i < (assumptions.size() - this.assumptions.size()) / this.repetitionAssumptions.size(); i++) {
				List<MetaFormula> metaAssumptions = repetitionAssumptionGenerate(i);
				for (int j = 0; j < this.repetitionAssumptions.size(); j++) {
					Formula assumption = assumptions.get(this.assumptions.size() + i * this.repetitionAssumptions.size() + j);
					MetaFormula metaAssumption = metaAssumptions.get(j);
					result = metaAssumption.isMatchedBy(assumption, result, context);
					if (result.isEmpty()) {
						return new HashSet<>();
					}
				}
			}
		}
		Set<Formula> subRes = new HashSet<>();
		for (MatchConstraint con: result) {
			try {
				int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 0;
				int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 1;
				context.put("maxIndex", maxIndex);
				context.put("maxDepth", maxDepth);
				subRes.add(conclusion.substitution(con.getBinding(), context));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return subRes;
	}
	
	public int getAssumptionSize() {
		return this.assumptions.size();
	}
	
	protected List<MetaFormula> repetitionAssumptionGenerate(int i) {
//		if (i == 0) {
//			return new ArrayList<>(this.repetitionAssumptions);
//		}
		List<MetaFormula> result = new ArrayList<>();
		for (MetaFormula metaFormula : this.repetitionAssumptions) {
			Map<MetaVariable, MetaRDLTerm> mapping = new HashMap<>();
			for (MetaVariable variable : metaFormula.getAllVariables()) {
				mapping.put(variable, variable.cloneWithName(variable.getVariableName().getName() + i));
			}
			result.add(metaFormula.replace(mapping));
		}
		return result;
	}
	
	
	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();
	}
	
}