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

import exceptions.SubstituteFailedException;
import inference.EquationAxiom;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.formulas.meta.MetaFormula;
import models.terms.meta.MatchConstraint;
import models.terms.meta.MetaDependencyTerm;
import models.terms.meta.MetaDynamicDependencyTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;

public class RightSubstitution extends EquationAxiom {

	public RightSubstitution() {
		super("Right Substitution");
		this.assumptions = new ArrayList<>();
		this.repetitionAssumptions = new ArrayList<>();
		assumptions.add(new MetaEquationFormula(
				new MetaEvaluatableTermVariable(new Variable("te0")),
				new MetaEvaluatableTermVariable(new Variable("ue0"))
		));
		repetitionAssumptions.add(new MetaDependencyFormula(
				new MetaEvaluatableTermVariable(new Variable("se")), 
				new MetaEvaluatableTermVariable(new Variable("re")) 
		));
		repetitionAssumptions.add(new MetaEquationFormula(
				new MetaDependencyTerm(
						new MetaEvaluatableTermVariable(new Variable("re")),
						new MetaEvaluatableTermVariable(new Variable("x")),
						new MetaEvaluatableTermVariable(new Variable("y"))
				),
				new MetaEvaluatableTermVariable(new Variable("te"))
		));
		conclusion = new MetaEquationFormula(
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								curIndex -= 1;
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2));
								}
								return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("se0"))
				),
				new MetaDynamicDependencyTerm(
						new MetaTermGenerator() {
							@Override
							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
								curIndex -= 1;
								if (curIndex % 2 == 0) {
									return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2));
								}
								if (curIndex == 1) {
									return new MetaEvaluatableTermVariable(new Variable("ue0"));
								}
								return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
							}
						},
						new MetaEvaluatableTermVariable(new Variable("se0"))
				)
		);
		conclusionMaxIndexCalculator = (assumptions) -> (assumptions.size() - 1) / 2 * 2 + 1; 
		conclusionMaxDepthCalculator = (assumptions) -> 1;
		assumptionRepetitionSizeCalculator = (conclusion) -> (conclusion.getMaxIndex() - 1) / 2;
	}
	
	@Override
	protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
		Set<MatchConstraint> result = new HashSet<>();
		result.add(constraint);
		for (int i = 0; i < this.assumptions.size(); i++) {
			MetaFormula metaAssumption = this.assumptions.get(i);
			Formula assumption = assumptions.get(i);
			result = metaAssumption.isMatchedBy(assumption, result);
			if (result.isEmpty()) {
				return new HashSet<>();
			}
		}
		if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) {
			return new HashSet<>();
		}
		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);
				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) : 0;
				subRes.add(conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth)));
			} catch (SubstituteFailedException e) {
				continue;
			}
		}
		return subRes;
	}
	
//	@Override
//	public RDLTerm generateRightSideHand(List<Formula> assumptions, RDLTerm leftSideHand) {
//		MetaRDLTerm metaLeftSideHand = ((MetaEquationFormula) conclusion).getLeftSideHand();
//		Set<MatchConstraint> result = metaLeftSideHand.isMatchedBy(leftSideHand);
//		int assumptionsSize = assumptionRepetitionSizeCalculator.calculate(leftSideHand);
//		for (int i = 0; i < this.assumptions.size(); i++) {
//			Formula assumption = assumptions.get(i);
//			MetaFormula metaAssumption = this.assumptions.get(i);
//			result = metaAssumption.isMatchedBy(assumption, result);
//			if (result.isEmpty()) {
//				return  null;
//			}
//		}
//		if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) {
//			return null;
//		}
//		for (int i = 0; i < assumptionsSize; i++) {
//			List<MetaFormula> metaAssumptions = repetitionAssumptionGenerate(i);
//			for (int j = 0; j < metaAssumptions.size(); j++) {
//				Formula assumption = assumptions.get(this.assumptions.size() + i * this.repetitionAssumptions.size() + j);
//				MetaFormula metaAssumption = metaAssumptions.get(j);
//				result = metaAssumption.isMatchedBy(assumption, result);
//				if (result.isEmpty()) {
//					return null;
//				}
//			}
//		}
//		return ((MetaEquationFormula) conclusion).getRightSideHand().substitute(result.iterator().next().getBinding(), Map.of("maxIndex", leftSideHand.getMaxIndex(), "maxDepth", leftSideHand.getMaxDepth()));
//	}
	
}