package inference;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Deque;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.stream.Collectors;

import models.algebra.Variable;
import models.formulas.DependencyFormula;
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.MetaEvaluatableTermVariable;

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 RightSubstitution();
//	
//	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
	);
	
	public static void debug() {
		for (var axiom : axioms) {
			System.out.println(axiom);
			System.out.println("==================================================================================================");
		}
	}
	
	record AxiomResult(InferenceRule axiom, List<Formula> formulas) {}
	
	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
		
		Map<Formula, AxiomResult> proofGraph = new HashMap<>();
		Map<InferenceRule, Set<List<Formula>>> appliedFormulas = new HashMap<>(); 
		
		for (InferenceRule axiom : axioms) {
			appliedFormulas.put(axiom, new HashSet<>());
		}
		
		Set<Formula> appearFormulas = new HashSet<>(assumptions);
		Set<RDLTerm> existTerms = new HashSet<>();
		for (Formula assumption : assumptions) {
			addExistTerms(assumption, existTerms);
		}
		int prevAppearFormulasSize = appearFormulas.size();
		while (! appearFormulas.contains(conclusion)) {
			Set<Formula> derivedFormulas = new HashSet<>();
			for(InferenceRule axiom : axioms) {
				derivedFormulas.addAll(applyAxiom(axiom, appearFormulas, appliedFormulas.get(axiom), existTerms, proofGraph));
			}
			if (derivedFormulas.size() == 0) {
				return false;
			}
			appearFormulas.addAll(derivedFormulas);
			if (appearFormulas.size() == prevAppearFormulasSize) {
				return false;
			}
			prevAppearFormulasSize = appearFormulas.size();
		}
		
		Queue<Formula> formulaQueue = new ArrayDeque<>();
		Queue<Integer> depthQueue = new ArrayDeque<>();
		List<Formula> formulaResult = new ArrayList<>();
		List<Integer> depthResult = new ArrayList<>();
		Set<Formula> used = new HashSet<>();
		Map<Integer, Set<InferenceRule>> usedAxioms = new HashMap<>();
		
		formulaQueue.add(conclusion);
		depthQueue.add(0);
		
		System.out.println("proof finish");
		System.out.println();
		
		while (formulaQueue.size() != 0) {
			Formula currentFormula = formulaQueue.poll();
//			if (used.contains(currentFormula)) {
//				continue;
//			}
			used.add(currentFormula);
			int currentDepth = depthQueue.poll();
			formulaResult.add(currentFormula);
			depthResult.add(currentDepth);
			if (! proofGraph.containsKey(currentFormula)) continue;
			for (Formula nextFormula : proofGraph.get(currentFormula).formulas) {
//				if (used.contains(nextFormula)) {
//					continue;
//				}
				formulaQueue.add(nextFormula);
				depthQueue.add(currentDepth + 1);
				if (! usedAxioms.containsKey(currentDepth + 1)) {
					usedAxioms.put(currentDepth + 1, new HashSet<>());
				}
				usedAxioms.get(currentDepth + 1).add(proofGraph.get(currentFormula).axiom);
			}
		}
		int prevDepth = depthResult.get(depthResult.size() - 1);
		Set<Formula> sameDepthFormulas = new HashSet<>();
		for (int i = formulaResult.size() - 1; i >= 0; i--) {
			int currentDepth = depthResult.get(i);
			Formula currentFormula = formulaResult.get(i);
			if (currentDepth != prevDepth) {
				String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(", "));
				String axioms = usedAxioms.get(prevDepth).stream().map(InferenceRule::getName).collect(Collectors.joining(", "));
				System.out.println(out);
				System.out.println("==============================================================(" + axioms + ")");
				sameDepthFormulas.clear();
			}
			prevDepth = currentDepth;
			sameDepthFormulas.add(currentFormula);
			
		}
		String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(","));
		System.out.println(out);
		return true;
	}
	
	private static Set<Formula> applyAxiom(InferenceRule axiom, Set<Formula> formulas, Set<List<Formula>> appliedFormulas,  Set<RDLTerm> existTerms, Map<Formula, AxiomResult> proofGraph) {
		Set<Formula> result = new HashSet<>();
//		List<List<Formula>> matchedFormulas = new ArrayList<>();
//		for (int i = 0; i < axiom.getAssumptionSize(); i++) {
//			matchedFormulas.add(new ArrayList<>());
//			for (Formula formula : formulas) {
//				if (! axiom.getAssumptions().get(i).isMatchedBy(formula).isEmpty()) {
//					matchedFormulas.get(i).add(formula);
//				}
//			}
//		}
//		for(List<Formula> applyFormulas : Product.product(matchedFormulas)) {
//			if (appliedFormulas.contains(applyFormulas)) continue;
//			Set<Formula> applied = axiom.apply(applyFormulas);
//			if (applied != null) {
//				for (Formula formula : applied) {
//					if (! formulas.contains(formula)) {
//						addExistTerms(formula, existTerms);
//						proofGraph.put(formula, new AxiomResult(axiom, applyFormulas));
//					}
//				}
//				result.addAll(applied);
//				appliedFormulas.add(applyFormulas);
//			}
//		}
		return result;
	}
	
	private static void addExistTerms(Formula formula, Set<RDLTerm> existTerms) {
		if (formula instanceof EquationFormula) {
			RDLTerm leftSideHand = ((EquationFormula) formula).getLeftSideHand();
			RDLTerm rightSideHand = ((EquationFormula) formula).getRightSideHand();
			existTerms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values());
			existTerms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values());
		} else if (formula instanceof DependencyFormula) {
			RDLTerm dependency = ((DependencyFormula) formula).getDependency();
			existTerms.addAll(dependency.getSubTerms(RDLTerm.class).values());
		} 
	}
	
	private static boolean equationTransitionCheck(Collection<Formula> assumptions, Formula conclusion) {
		if (! (conclusion instanceof EquationFormula)) {
			return false;
		}
		EquationFormula equationConclusion = (EquationFormula) conclusion;
		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = constructEquationGraph(assumptions);
		Deque<EvaluatableTerm> que = new ArrayDeque<>();
		Set<EvaluatableTerm> visited = new HashSet<>();
		que.add(equationConclusion.getLeftSideHand());
		while (! que.isEmpty()) {
			EvaluatableTerm curNode = que.pollFirst();
			if (curNode.equals(equationConclusion.getRightSideHand())) {
				return true;
			}
			for (EvaluatableTerm nextNode : graph.getOrDefault(curNode, new ArrayList<>())) {
				if (visited.contains(nextNode)) {
					continue;
				}
				visited.add(nextNode);
				que.add(nextNode);
			}
		}
		return false;
	}
	
	private static Map<EvaluatableTerm, List<EvaluatableTerm>> constructEquationGraph(Collection<Formula> assumptions) {
		List<EquationFormula> equations = new ArrayList<>();
		for (Formula assumption : assumptions) {
			if (assumption instanceof EquationFormula) {
				equations.add((EquationFormula) assumption);
			}
		}
		
		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = new HashMap<>();
		for (EquationFormula equation : equations) {
			EvaluatableTerm lsh = equation.getLeftSideHand();
			EvaluatableTerm rsh = equation.getRightSideHand();
			if (! graph.containsKey(lsh)) {
				graph.put(lsh, new ArrayList<>());
			}
			if (! graph.containsKey(rsh)) {
				graph.put(rsh, new ArrayList<>());
			}
			graph.get(lsh).add(rsh);
			graph.get(rsh).add(lsh);
		}
		return graph;
	}
}