package inference.rewrite;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

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 boolean inference() {
		Map<Resource, List<Resource>> resourceTree = new HashMap<>();
		Resource root = parseDependencyTerm(inputFormula.getLeftSideHand(), resourceTree, new ArrayList<>());
		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<EvaluatableTerm> dependedTerms = depTerm.getDependedTerms();
		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 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;
	}
	
	
}