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 com.google.common.collect.BoundType;

import models.algebra.Variable;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.Dependency;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import models.terms.meta.MetaDynamicDependency;
import models.terms.meta.MetaDynamicDependencyTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaTermGenerator;

public class ProofSystem {

	//======================Equality Axioms=============================
	
	public static final InferenceRule reflexivity = new InferenceRule(
			"Reflexivity",
			List.of(),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("te")), 
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	public static final InferenceRule symmetry = new InferenceRule(
			"Symmetry",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")), 
							new MetaEvaluatableTermVariable(new Variable("se"))
					)
			),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("se")), 
					new MetaEvaluatableTermVariable(new Variable("te"))
			)
	);
	
	public static final InferenceRule transitivity = new InferenceRule(
			"Transitivity",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("se")), 
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")), 
							new MetaEvaluatableTermVariable(new Variable("ue"))
					)
			),
			new MetaEquationFormula(
					new MetaEvaluatableTermVariable(new Variable("se")), 
					new MetaEvaluatableTermVariable(new Variable("ue"))
			)
			
	);
	
	public static final InferenceRule rightSubstitution = new InferenceRule(
			"Right Substitution",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("ue")),
							new MetaEvaluatableTermVariable(new Variable("ve"))
					),
					new MetaDependencyFormula(
							new MetaDynamicDependency(
									new MetaTermGenerator() {
										@Override
										public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
											curIndex -= 2;
											return new MetaEvaluatableTermVariable(new Variable("te" + curIndex));
										}
									},
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					)
			),
			new MetaEquationFormula(
					new MetaDynamicDependencyTerm(
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
									curIndex -= 3;
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
									}
									return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
								}
							},
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaDynamicDependencyTerm(
							new MetaTermGenerator() {
								@Override
								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
									curIndex -= 3;
									if (curIndex % 2 == 0) {
										return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
									}
									return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2));
								}
							},
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaEvaluatableTermVariable(new Variable("ve"))
					)
			)
	);
//	
//	public static final InferenceRule leftSubstitution = new EquationAxiom(
//			"Left Substitution",
//			List.of(
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					)
//			),
//			List.of(
//					new MetaDependencyFormula(
//							new MetaEvaluatableTermVariable(new Variable("se")), 
//							new MetaEvaluatableTermVariable(new Variable("re")) 
//					),
//					new MetaEquationFormula(
//							new MetaDependencyTerm(
//									new MetaEvaluatableTermVariable(new Variable("re")),
//									new MetaEvaluatableTermVariable(new Variable("x")),
//									new MetaEvaluatableTermVariable(new Variable("y"))
//							),
//							new MetaEvaluatableTermVariable(new Variable("ue"))
//					)
//			),
//			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("ue" + curIndex / 2));
//								}
//							},
//							new MetaEvaluatableTermVariable(new Variable("se"))
//					),
//					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("ue" + curIndex / 2));
//								}
//							},
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					)
//			),
//			null,
//			(assumptions) -> (assumptions.size() - 1) / 2 * 2 + 1,
//			(assumptions) -> 1,
//			(conclusion) -> (conclusion.getMaxIndex() - 1) / 2
//	);
//	

//	public static final InferenceRule identity = new EquationAxiom(
//			"Identity",
//			List.of(),
//			List.of(
//				new MetaEquationFormula(
//							new MetaDependencyTerm(
//									new MetaEvaluatableTermVariable(new Variable("se")),
//									new MetaEvaluatableTermVariable(new Variable("x")),
//									new MetaEvaluatableTermVariable(new Variable("y"))
//							),
//							new MetaEvaluatableTermVariable(new Variable("te"))
//					)
//			),
//			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("se" + curIndex / 2));
//									}
//									return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
//								}
//								
//							},
//							new MetaEvaluatableTermVariable(new Variable("se0"))
//					),
//					new MetaEvaluatableTermVariable(new Variable("te0"))
//			),
//			null,
//			(assumptions) -> assumptions.size() * 2 + 1,
//			(assumptions) -> 1,
//			(conclusion) -> (conclusion.getMaxIndex() - 1) / 2
//	);
//	
//	public static final InferenceRule mapComposition = new MapComposition();
//	
//	public static final InferenceRule constantness = new Constantness();
//	
//	public static final InferenceRule rightNormalization = new RightNormalization();
//	
//	public static final InferenceRule pseudoConstantness = new InferenceRule(
//			"Pseudo-Constantness",
//			List.of(
//					new MetaDependencyFormula(
//							new MetaDynamicDependency(
//									(ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1)), new Variable("n")),
//									new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
//							)
//					)
//			),
//			List.of(),
//			new MetaEquationFormula(
//					new MetaDynamicDependencyTerm(
//							(ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1) / 2), new Variable("n")),
//							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
//					),
//					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
//			),
//			new InferenceOrderConstraint(new Constant("0"), OrderConstraint.GT, new Variable("n")),
//			(assumptions) -> (((DependencyFormula)assumptions.get(0)).getDependency().getMaxIndex() - 1) * 2 + 1,
//			(assumptions) -> 1,
//			(term) -> (term.getMaxIndex() - 1) / 2 + 1
//	);
	
//	public static final InferenceRule uncurrying = new Uncurrying();
//	
//	public static final InferenceRule argumentDependencyExtraction = new ArgumentDependencyExtraction();
	
	
//	
//	//======================Dependency Axioms=============================
//	

//	public static final InferenceRule identityMapping = new InferenceRule(
//			"Identity Mapping",
//			List.of(
//					new MetaEquationFormula(
//							new MetaEvaluatableTermVariable(new Variable("te")),
//							new MetaEvaluatableTermVariable(new Variable("se"))
//					)
//			),
//			List.of(),
//			new MetaDependencyFormula(
//					new MetaEvaluatableTermVariable(new Variable("te")),
//					new MetaEvaluatableTermVariable(new Variable("se"))
//			),
//			null,
//			null,
//			null,
//			null
//	);
	
//	public static final InferenceRule compositeMapping = new CompositeMapping();
	
//	public static final InferenceRule constantMapping = new InferenceRule(
//			"Constant Mapping",
//			List.of(),
//			List.of(),
//			new MetaDependencyFormula(
//					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
//					new MetaEvaluatableTermVariable(new Variable("re"), new Variable("m"))
//			),
//			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")),
//			null,
//			null,
//			null
//	);
	
//	public static final InferenceRule uncurriedMapping = new UncurriedMapping();
	
//	public static final InferenceRule redundantDependency  = new InferenceRule(
//			"Redundant Dependency",
//			List.of(
//					new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")))
//			),
//			List.of(),
//			new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("p"), ExpressionUtils.parse("n - 1"))),
//			null,
//			null,
//			null,
//			null
//	);
	
//	public static final InferenceRule redundancyElimination = new RedundancyElimination();
	
	/*
	 * new InferenceRule(
			"",
			List.of(),
			List.of(),
			null,
			null,
			null,
			null,
			null
	);
	 */
	
	
	private static final List<InferenceRule> axioms = List.of(
//			reflexivity, 
//			symmetry, 
//			transitivity,
//			rightSubstitution, 
//			leftSubstitution, 
//			identity, 
//			mapComposition, 
//			constantness,
//			rightNormalization,
//			pseudoConstantness,
//			identityMapping,
//			compositeMapping,
//			constantMapping,
//			slicedMapping,
//			memberSubstitution, 
//			membershipChain, 
//			collectionSubstitution,
//			setEquivelence,
//			setHomomorphism,
//			leftProjection,
//			rightProjection,
//			domainMembership,
//			codomainMembership,
//			codomainMembership2
	);
	

	private Set<DependencyFormula> dependencyFormulas = new HashSet<>();
	private Set<EquationFormula> equationFormulas = new HashSet<>();
	private Map<DependencyFormula, List<Set<In>>> dependencyInMap = new HashMap<>();
	private Map<EvaluatableTerm, Set<In>> ins = new HashMap<>();
	private Set<RDLTerm> terms = new HashSet<>();
	
	public void addDependency(Dependency dependency) {
		addDependency(new DependencyFormula(dependency));
	}
	
	public void addDependency(DependencyFormula dependency) {
		dependencyFormulas.add(dependency);
		addExistTerms(dependency);
		Dependency dep = dependency.getDependency();
		dependencyInMap.put(dependency, new ArrayList<>());
		for (EvaluatableTerm dependedTerm : dep.getDependedTerms()) {
			if (ins.containsKey(dependedTerm)) {
				dependencyInMap.get(dependency).add(new HashSet<>(ins.get(dependedTerm)));
			} else {
				dependencyInMap.get(dependency).add(new HashSet<>());
			}
		}
	}
	
	public void addEquationFormula(EquationFormula eq) {
		addExistTerms(eq);
		equationFormulas.add(eq);
		Set<In> ins = In.deriveIn(eq);
		for (In in : ins) {
			this.ins.computeIfAbsent(in.getRightSideHand(), t -> new HashSet<>()).add(in);
			for (DependencyFormula depFormula : dependencyInMap.keySet()) {
				int startIndex = depFormula.getDependency().getDependedTerms().headMultiset(in.getRightSideHand(), BoundType.OPEN).size();
				int count = depFormula.getDependency().getDependedTerms().count(in.getRightSideHand());
				for (int i = 0; i < count; i++) {
					dependencyInMap.get(depFormula).get(startIndex + i).add(in);
				}
			}
		}
	}
	
	private void dependencyInMap(DependencyFormula key, int index, In in) {
		
	}
	
	
	private void addExistTerms(Formula formula) {
		if (formula instanceof EquationFormula) {
			RDLTerm leftSideHand = ((EquationFormula) formula).getLeftSideHand();
			RDLTerm rightSideHand = ((EquationFormula) formula).getRightSideHand();
			terms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values());
			terms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values());
		} else if (formula instanceof DependencyFormula) {
			RDLTerm dependency = ((DependencyFormula) formula).getDependency();
			terms.addAll(dependency.getSubTerms(RDLTerm.class).values());
		} 
	}
	
}