package inference.rewrite;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Deque;
import java.util.List;
import java.util.Map;

import inference.rewrite.ResourceTree;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.Then;
import models.terms.DependencyTerm;
import models.terms.EvaluatableTerm;
import models.terms.PrimedTerm;
import models.terms.Resource;

public class RewriteInferenceSystem {

	List<Formula> constraintFormulas = new ArrayList<>();
	List<Formula> invariantFormulas = new ArrayList<>();
	EquationFormula inputFormula;
	List<Formula> conditionalFormulas = new ArrayList<>();
	List<Formula> otherFormulas = new ArrayList<>();
	Formula conclusion;
	
	
	public RewriteInferenceSystem(List<Formula> assumptions, Formula conclusion) {
		for (Formula assumption : assumptions) {
			if (inputFormulaCheck(assumption)) {
				inputFormula = (EquationFormula) assumption;
			} else if(invariantFormulaCheck(assumption)) {
				invariantFormulas.add(assumption);
			} else if (assumption instanceof EquationFormula) {
				constraintFormulas.add(assumption);
			} else {
				otherFormulas.add(assumption);
			}
		}
		
		if (conclusion instanceof Then then) {
			conditionalFormulas.add(then.getCondition());
			this.conclusion = then.getResult();
		} else {
			this.conclusion = conclusion;
		}
		
	}
	
	public void debug() {
		System.out.println("constraintFormulas: " + constraintFormulas.toString());
		System.out.println("invariantFormulas: " + invariantFormulas.toString());
		System.out.println("inputFormula: " + inputFormula.toString());
		System.out.println("conditionalFormulas: " + conditionalFormulas.toString());
		System.out.println("conclusion: " + conclusion.toString());
	}
	
	public boolean inference() {
//		Map<Resource, List<Resource>> inputFormulaTree = new HashMap<>();
//		Resource root = parseDependencyTerm(inputFormula.getLeftSideHand(), inputFormulaTree, new ArrayList<>());
//		ResourceTree inputResourceTree = new ResourceTree(root, inputFormulaTree);
//		List<ResourceTree> otherRoots = new ArrayList<>();
//		for (Formula formula : constraintFormulas) {
//			if (formula instanceof EquationFormula equation) {
//				Map<Resource, List<Resource>> resourceTree = new HashMap<>();
//				Resource treeRoot = parseDependencyTerm(equation.getRightSideHand(), resourceTree, new ArrayList<>());
//				otherRoots.add(new ResourceTree(treeRoot, resourceTree));
//			}
//		}
//		for (Formula formula : conditionalFormulas) {
//			if (formula instanceof EquationFormula equation) {
//				Map<Resource, List<Resource>> resourceTree = new HashMap<>();
//				Resource treeRoot = parseDependencyTerm(equation.getLeftSideHand(), resourceTree, new ArrayList<>());
//				otherRoots.add(new ResourceTree(treeRoot, resourceTree));
//			}
//		}
//		System.out.println(inputResourceTree);
		return false;
	}
	
	private Resource parseDependencyTerm(EvaluatableTerm term, Map<Resource, List<Resource>> resourceTree, List<Resource> tops) {
		if (term instanceof Resource resource) {
			if (tops.isEmpty()) {
				resourceTree.put(resource, new ArrayList<>());
				tops.add(resource);
			} else {
				for (Resource top : tops) {
					resourceTree.get(top).add(resource);
					resourceTree.put(resource, new ArrayList<>());
				}
				tops.clear();
				tops.add(resource);
			}
			return resource;
		}
		Resource root;
		DependencyTerm depTerm = (DependencyTerm) term;
		EvaluatableTerm dependingTerm = depTerm.getDependingTerm();
		List<Resource> dependedTerms = depTerm.getDependedResources();
		List<EvaluatableTerm> argumentTerms = depTerm.getArgumentTerms();
		root = parseDependencyTerm(dependingTerm, resourceTree, tops);
		List<Resource> nextTops = new ArrayList<>();
		for (int i = 0; i < dependedTerms.size(); i++) {
			List<Resource> currentTops = new ArrayList<>(tops);
			parseDependencyTerm(dependedTerms.get(i), resourceTree, currentTops);
			parseDependencyTerm(argumentTerms.get(i), resourceTree, currentTops);
			nextTops.addAll(currentTops);
		}
		tops.clear();
		tops.addAll(nextTops);
		return root;
	}
	
//	private Map<Resource, List<Resource>> joinTree(Map<Resource, List<Resource>> baseTree, Map<Resource, List<Resource>> joinTree) {
//		
//	}
//	
	private ResourceTree joinTreeLeft(ResourceTree baseTree, ResourceTree joinTree) {
		
//		ResourceTree result = new ResourceTree(baseTree.root(), new HashMap<>(baseTree.tree()));
//		
//		Deque<Resource> curRootQue = new ArrayDeque<>();
//		curRootQue.add(joinTree.root());
//		
//		while (! curRootQue.isEmpty()) {
//			Resource curRoot = curRootQue.pollFirst();
//			if (isTreeMatch(result.tree(), curRoot, joinTree.tree())) {
//				
//			}
//			curRootQue.addAll(joinTree.tree.get(curRoot));
//		}
		
//		return result;
		return null;
	}
	
	private boolean isTreeMatch(Map<Resource, List<Resource>> baseTree, Resource joinRoot, Map<Resource, List<Resource>> joinTree) {
		Deque<Resource> joinCurResourceStack = new ArrayDeque<>();
		joinCurResourceStack.add(joinRoot);
		while (! joinCurResourceStack.isEmpty()) {
			Resource joinCurResource = joinCurResourceStack.pollLast();
			if (! baseTree.keySet().contains(joinCurResource)) {
				return false;
			}
			if (! baseTree.get(joinCurResource).equals(joinTree.get(joinCurResource))) {
				return false;
			}
			joinCurResourceStack.addAll(joinTree.get(joinCurResource));
		}
		
		return true;
	}
	
	private boolean inputFormulaCheck(Formula formula) {
		if (! (formula instanceof EquationFormula equation)) {
			return false;
		}
		List<Resource> resources  = new ArrayList<>(equation.getLeftSideHand().getSubTerms(Resource.class).values());
		resources.addAll(equation.getRightSideHand().getSubTerms(Resource.class).values());
		for (Resource resource : resources) {
			if (resource.getOrder() == 0) {
				return true;
			}
		}
		return false;
	}
	
	private boolean invariantFormulaCheck(Formula formula) {
		if (! (formula instanceof EquationFormula equation)) {
			return false;
		}
		EvaluatableTerm leftSideHand = equation.getLeftSideHand();
		EvaluatableTerm rightSideHand = equation.getRightSideHand();
		
		if (leftSideHand instanceof PrimedTerm) {
			return ((PrimedTerm) leftSideHand).getPrimedTerm().equals(rightSideHand);
		} else if (rightSideHand instanceof PrimedTerm) {
			return ((PrimedTerm) rightSideHand).getPrimedTerm().equals(leftSideHand);
		}
		
		return false;
	}
	
	
}