package inference;

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

import lombok.Getter;
import lombok.RequiredArgsConstructor;
import models.algebra.Variable;
import models.formulas.EquationFormula;
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.MetaConstant;
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;


@RequiredArgsConstructor
@Getter
public class In extends Formula {
	
	private final EvaluatableTerm leftSideHand;
	private final EvaluatableTerm rightSideHand;
	
	static final MetaEquationFormula domainMembershipAssumption = new MetaEquationFormula(
			new MetaDynamicDependencyTerm(
					new MetaTermGenerator() {
						@Override
						public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<Object, Object> context) {
							context.put("" + curDepth, curIndex);
							if (curDepth == maxDepth - 1 && curIndex == 0) {
								return new MetaDependencyTerm(
										new MetaEvaluatableTermVariable(new Variable("se")),
										new MetaEvaluatableTermVariable(new Variable("te")),
										new MetaEvaluatableTermVariable(new Variable("ue"))
								);
							} else if (curIndex == 0) {
								return new MetaDynamicDependencyTerm(this);
							}
							curIndex -= 1;
							if (curIndex % 2 == 0) {
								return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex/2));
							}
							return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex/2));
						}
					}
			),
			new MetaConstant(new Variable("c"))
	);
	
	static final MetaDependencyTerm domainMembershipConclusionLeftSideHand = new MetaDynamicDependencyTerm(
			new MetaTermGenerator() {
				@Override
				public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<Object, Object> context) {
					maxIndex = (Integer) context.get("" + curDepth);
					if (curDepth == maxDepth && curIndex == 0) {
						return new MetaEvaluatableTermVariable(new Variable("ue"));
					}
					curIndex -= 1;
					if (curIndex >= maxIndex) {
						return null;
					}
					if (curIndex % 2 == 0) {
						return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex/2));
					}
					return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex/2));
				}
			}
	);
	
	static final MetaDependencyTerm domainMembershipConclusionRightSideHand = new MetaDynamicDependencyTerm(
			new MetaTermGenerator() {
				@Override
				public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<Object, Object> context) {
					maxIndex = (Integer) context.get("" + curDepth);
					if (curDepth == maxDepth && curIndex == 0) {
						return new MetaEvaluatableTermVariable(new Variable("te"));
					}
					curIndex -= 1;
					if (curIndex >= maxIndex) {
						return null;
					}
					if (curIndex % 2 == 0) {
						return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex/2));
					}
					return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex/2));
				}
			}
	);
	
	
	static final MetaEvaluatableTermVariable codomainMembershipConclusionLeftSideHand = new MetaEvaluatableTermVariable(new Variable("ve"));
	static final MetaEvaluatableTermVariable codomainMembershipConclusionRightSideHand = new MetaEvaluatableTermVariable(new Variable("se"));
	
	static final MetaEquationFormula codomainMembershipAssumption = new MetaEquationFormula(
			new MetaDynamicDependencyTerm(
					new MetaTermGenerator() {
						@Override
						public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<Object, Object> context) {
							curIndex -= 1;
							if (curIndex % 2 == 0) {
								return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
							}
							return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
						}
					},
					new MetaEvaluatableTermVariable(new Variable("se"))
			),
			new MetaEvaluatableTermVariable(new Variable("ve"))
	);
	
	public Set<MetaEquationFormula> deriveRule() {
		Set<MetaEquationFormula> result = new HashSet<>();
//		result.addAll(deriveByDomainMemberShip());
//		result.addAll(deriveByCodomainMemberShip());
		return result;
	}
	
	static Set<In> deriveIn(Set<EquationFormula> equationFormulas) {
		Set<In> result = new HashSet<>();
		for (EquationFormula eq : equationFormulas) {
			result.addAll(deriveByDomainMembership(eq));
			result.addAll(deriveByCodomainMembership(eq));
		}
		return result;
	}
	
	static Set<In> deriveIn(EquationFormula equationFormula) {
		return deriveIn(Set.of(equationFormula));
	}
	
	static Set<In> deriveByDomainMembership(EquationFormula equationFormula) {
		Set<In> result = new HashSet<>();
		Set<MatchConstraint> constraints = domainMembershipAssumption.isMatchedBy(equationFormula);
		for (MatchConstraint constraint : constraints) {
			constraint.getContext().put("maxDepth", equationFormula.getLeftSideHand().getMaxDepth() - 1);
			constraint.getContext().put("maxIndex", 10000);
			RDLTerm left = domainMembershipConclusionLeftSideHand.substitute(constraint.getBinding(), constraint.getContext());
			RDLTerm right = domainMembershipConclusionRightSideHand.substitute(constraint.getBinding(), constraint.getContext());
			result.add(new In((EvaluatableTerm) left, (EvaluatableTerm)right));
		}
		return result;
	}
	
	static Set<In> deriveByCodomainMembership(EquationFormula equationFormula) {
		Set<In> result = new HashSet<>();
		Set<MatchConstraint> constraints = codomainMembershipAssumption.isMatchedBy(equationFormula);
		for (MatchConstraint constraint : constraints) {
			RDLTerm left = codomainMembershipConclusionLeftSideHand.substitute(constraint.getBinding(), constraint.getContext());
			RDLTerm right = codomainMembershipConclusionRightSideHand.substitute(constraint.getBinding(), constraint.getContext());
			result.add(new In((EvaluatableTerm) left, (EvaluatableTerm)right));
		}
		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();
	}
	
}