package inference;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import lombok.Getter;
import lombok.RequiredArgsConstructor;
import models.algebra.Constant;
import models.algebra.Variable;
import models.formulas.Formula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
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.MetaResource;
import models.terms.meta.MetaTermGenerator;


@RequiredArgsConstructor
@Getter
public class In extends Formula {
	
	private final EvaluatableTerm leftSideHand;
	private final EvaluatableTerm rightSideHand;
	
	private static final MetaDependencyTerm domainMembershipConclusionLeftSideHand = new MetaDynamicDependencyTerm(
			new MetaTermGenerator() {
				@Override
				public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
					context.put("1-" + curDepth, curIndex);
					context.put("depth1", maxDepth);
					if (curDepth == maxDepth && curIndex == 0) {
						return new MetaEvaluatableTermVariable(new Variable("ue1"));
					} else if (curIndex == 0) {
						return new MetaDynamicDependencyTerm(this);
					} 
					int used = (Integer) context.getOrDefault("used1", 4);
					context.put("used1", used + 1);
					curIndex -= 1;
					if (curIndex % 2 == 0) {
						return new MetaEvaluatableTermVariable(new Variable("te" + used / 2));
					}
					return new MetaEvaluatableTermVariable(new Variable("ue" + used / 2));
				}
			}
	);
	
	private static final MetaDependencyTerm domainMembershipConclusionRightSideHand = new MetaDynamicDependencyTerm(
			new MetaTermGenerator() {
				@Override
				public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
					context.put("2-" + curDepth, curIndex);
					context.put("depth2", maxDepth);
					if (curDepth == maxDepth && curIndex == 0) {
						return new MetaEvaluatableTermVariable(new Variable("te1"));
					} else if (curIndex == 0) {
						return new MetaDynamicDependencyTerm(this);
					} 
					int used = (Integer) context.getOrDefault("used2", 4);
					context.put("used2", used + 1);
					curIndex -= 1;
					if (curIndex % 2 == 0) {
						return new MetaEvaluatableTermVariable(new Variable("te" + used / 2));
					}
					return new MetaEvaluatableTermVariable(new Variable("ue" + used / 2));
				}
			}
	);
	
	private static final MetaDynamicDependencyTerm domainMembershipAssumptionLeftSideHand = new MetaDynamicDependencyTerm(
			new MetaTermGenerator() {
				@Override
				public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
					if (curIndex - 1 >= (Integer) context.get("1-" + curDepth)) {
						return null;
					}
					if (curIndex == 0 && curDepth == maxDepth) {
						return new MetaDependencyTerm(
								new MetaEvaluatableTermVariable(new Variable("se")),
								new MetaEvaluatableTermVariable(new Variable("te1")),
								new MetaEvaluatableTermVariable(new Variable("ue1"))
						);
					}
					else if (curIndex == 0) {
						return new MetaDynamicDependencyTerm(this);
					}
					curIndex -= 1;
					int used = (Integer) context.getOrDefault("used3", 4);
					context.put("used3", used + 1);
					if (curIndex % 2 == 0) {
						return new MetaEvaluatableTermVariable(new Variable("te" + used / 2));
					}
					return new MetaEvaluatableTermVariable(new Variable("ue" + used / 2));
				}
			}
	);
	
	private static final MetaEvaluatableTermVariable codomainMembershipConclusionLeftSideHand = new MetaEvaluatableTermVariable(new Variable("ve"));
	private static final MetaEvaluatableTermVariable codomainMembershipConclusionRightSideHand = new MetaEvaluatableTermVariable(new Variable("se"));
	
	public Set<MetaEquationFormula> deriveRule() {
		Set<MetaEquationFormula> result = new HashSet<>();
		result.addAll(deriveByDomainMemberShip());
		result.addAll(deriveByCodomainMemberShip());
		return result;
	}
	
	private Set<MetaEquationFormula> deriveByDomainMemberShip() {
		Set<MetaEquationFormula> result = new HashSet<>();
		Set<MatchConstraint> leftMatchResult = domainMembershipConclusionLeftSideHand.isMatchedBy(leftSideHand);
		Set<MatchConstraint> rightMatchResult = domainMembershipConclusionRightSideHand.isMatchedBy(rightSideHand, leftMatchResult);
		for (MatchConstraint constraint: rightMatchResult) {
			int used1 = (Integer) constraint.getContext().getOrDefault("used1", 1);
			int used2 = (Integer) constraint.getContext().getOrDefault("used2", 1);
			int depth1 = (Integer) constraint.getContext().get("depth1");
			int depth2 = (Integer) constraint.getContext().get("depth2");
			if (used1 != used2) {
				continue;
			}
			if (depth1 != depth2) {
				continue;
			}
			boolean flg = false;
			for (int i = 1; i < depth1; i++) {
				int d1 = (Integer) constraint.getContext().get("1-" + i);
				int d2 = (Integer) constraint.getContext().get("2-" + i);
				if (d1 != d2) {
					flg = true;
					break;
				}
			}
			if (flg) continue;
			Map<MetaRDLTerm, RDLTerm> mapping = new HashMap<>();
			for (Variable variable: constraint.getBinding().keySet()) {
				mapping.put(new MetaEvaluatableTermVariable(variable), constraint.getBinding().get(variable));
			}
			MetaRDLTerm left = (MetaRDLTerm)domainMembershipAssumptionLeftSideHand.generate(10000, depth1, constraint.cloneContext()).replace(mapping);
			MetaResource right = new MetaResource(new Variable("c"), new Constant("0"));
			result.add(new MetaEquationFormula(left, right));
		}
		return result;
	}
	
	private Set<MetaEquationFormula> deriveByCodomainMemberShip() {
		Set<MetaEquationFormula> result = new HashSet<>();
		Set<MatchConstraint> leftMatchResult = codomainMembershipConclusionLeftSideHand.isMatchedBy(leftSideHand);
		Set<MatchConstraint> rightMatchResult = codomainMembershipConclusionRightSideHand.isMatchedBy(rightSideHand, leftMatchResult);
		for (MatchConstraint constraint : rightMatchResult) {
			Map<MetaRDLTerm, RDLTerm> mapping = new HashMap<>();
			for (Variable variable: constraint.getBinding().keySet()) {
				mapping.put(new MetaEvaluatableTermVariable(variable), constraint.getBinding().get(variable));
			}
			MetaRDLTerm left = 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("te" + curIndex / 2));
							}
							return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
						}
					},
					constraint.getBinding().get(codomainMembershipConclusionRightSideHand.getVariableName())
			);
			result.add(new MetaEquationFormula(left, constraint.getBinding().get(codomainMembershipConclusionLeftSideHand.getVariableName())));
		}
		return result;
	}
	
	@Override
	public String toString() {
		return leftSideHand.toString() + " in " + rightSideHand.toString();
	}
	
	@Override
	public boolean equals(Object another) {
		if (another instanceof In in) {
			return this.leftSideHand.equals(in.getLeftSideHand()) && this.rightSideHand.equals(in.getRightSideHand());
		}
		return false;
	}
	
	@Override
	public int hashCode() {
		return toString().hashCode();
	}
	
}