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 exceptions.MissingContextException;
import lombok.Getter;
import models.formulas.DependencyFormula;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.meta.MetaEquationFormula;
import models.terms.Dependency;
import models.terms.EvaluatableTerm;
import models.terms.RDLTerm;
import models.terms.meta.MetaRDLTerm;

@Getter
public class ProofState {

	private Set<Dependency> dependencies = new HashSet<>();
	private Set<EvaluatableTerm> evaluatableTerms = new HashSet<>();
	private Set<Formula> formulas = new HashSet<>();
	private Set<DependencyFormula> dependencyFormulas = new HashSet<>();
	private Set<EquationFormula> equationFormulas = new HashSet<>();
 	private Map<InferenceRule, List<Set<Formula>>> matchedFormulas = new HashMap<>();
 	private Map<EquationAxiom, ConclusionMatchedTerm> matchedTerms = new HashMap<>();
 	private InferenceHistory history = new InferenceHistory();
 	
	public ProofState(Set<Formula> existFormulas) {
		for (Formula formula: existFormulas) {
			formulas.add(formula);
			if (formula instanceof DependencyFormula df) {
				this.dependencyFormulas.add(df);
				this.dependencies.add(df.getDependency());
				this.evaluatableTerms.addAll(df.getDependency().getSubTerms(EvaluatableTerm.class).values());
			} else if (formula instanceof EquationFormula eq) {
				this.equationFormulas.add(eq);
				this.evaluatableTerms.addAll(eq.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values());
				this.evaluatableTerms.addAll(eq.getRightSideHand().getSubTerms(EvaluatableTerm.class).values());
			}
		}
		for (InferenceRule rule: ProofSystem.dependencyAxioms) {
			List<Set<Formula>> terms = new ArrayList<>();
			for (int i = 0; i < rule.getAssumptionSize(); i++) {
				terms.add(new HashSet<>());
				for (DependencyFormula dep : dependencyFormulas) {
					if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) {
						terms.get(i).add(dep);
					}
				}
				for (EquationFormula eq : equationFormulas) {
					if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) {
						terms.get(i).add(eq);
					}
				}
			}
			matchedFormulas.put(rule, terms);
		}
		for (EquationAxiom rule: ProofSystem.equationAxioms) {
			List<Set<Formula>> formulas = new ArrayList<>();
			MetaRDLTerm conclusionLeft = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getLeftSideHand();
			MetaRDLTerm conclusionRight = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getRightSideHand();
			Set<EvaluatableTerm> lhs = new HashSet<>();
			Set<EvaluatableTerm> rhs = new HashSet<>();
			for (EvaluatableTerm term : evaluatableTerms) {
				try {
					if (! conclusionLeft.isMatchedBy(term).isEmpty()) {
						lhs.add(term);
					}
				} catch (RuntimeException e) {}
				try {
					if (! conclusionRight.isMatchedBy(term).isEmpty()) {
						rhs.add(term);
					}
				} catch(RuntimeException e) {}
			}
			matchedTerms.put(rule, new ConclusionMatchedTerm(lhs, rhs));
			for (int i = 0; i < rule.getAssumptionSize(); i++) {
				formulas.add(new HashSet<>());
				for (DependencyFormula dep : dependencyFormulas) {
					if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) {
						formulas.get(i).add(dep);
					}
				}
				for (EquationFormula eq : equationFormulas) {
					if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) {
						formulas.get(i).add(eq);
					}
				}
			}
			matchedFormulas.put(rule, formulas);
		}
 	}
	
	public void addFormuals(Set<? extends Formula> existFormulas) {
		for (Formula formula: existFormulas) {
			formulas.add(formula);
			if (formula instanceof DependencyFormula df) {
				this.dependencyFormulas.add(df);
				this.dependencies.add(df.getDependency());
				this.evaluatableTerms.addAll(df.getDependency().getSubTerms(EvaluatableTerm.class).values());
			} else if (formula instanceof EquationFormula eq) {
				this.equationFormulas.add(eq);
				this.evaluatableTerms.addAll(eq.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values());
				this.evaluatableTerms.addAll(eq.getRightSideHand().getSubTerms(EvaluatableTerm.class).values());
			}
		}
		for (InferenceRule rule: ProofSystem.dependencyAxioms) {
			List<Set<Formula>> terms = new ArrayList<>();
			for (int i = 0; i < rule.getAssumptionSize(); i++) {
				terms.add(new HashSet<>());
				for (DependencyFormula dep : dependencyFormulas) {
					if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) {
						terms.get(i).add(dep);
					}
				}
				for (EquationFormula eq : equationFormulas) {
					if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) {
						terms.get(i).add(eq);
					}
				}
			}
			matchedFormulas.put(rule, terms);
		}
		for (EquationAxiom rule: ProofSystem.equationAxioms) {
			List<Set<Formula>> formulas = new ArrayList<>();
			MetaRDLTerm conclusionLeft = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getLeftSideHand();
			MetaRDLTerm conclusionRight = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getRightSideHand();
			Set<EvaluatableTerm> lhs = new HashSet<>();
			Set<EvaluatableTerm> rhs = new HashSet<>();
			for (EvaluatableTerm term : evaluatableTerms) {
				try {
					if (! conclusionLeft.isMatchedBy(term).isEmpty()) {
						lhs.add(term);
					}
				} catch (MissingContextException e) {}
				try {
					if (! conclusionRight.isMatchedBy(term).isEmpty()) {
						rhs.add(term);
					}
				} catch (MissingContextException e) {}
			}
			matchedTerms.put(rule, new ConclusionMatchedTerm(lhs, rhs));
			for (int i = 0; i < rule.getAssumptionSize(); i++) {
				formulas.add(new HashSet<>());
				for (DependencyFormula dep : dependencyFormulas) {
					if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) {
						formulas.get(i).add(dep);
					}
				}
				for (EquationFormula eq : equationFormulas) {
					if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) {
						formulas.get(i).add(eq);
					}
				}
			}
			matchedFormulas.put(rule, formulas);
		}
	}
	
	public void addHistory(List<Formula> assumptions, InferenceRule usedAxiom, Formula conclusion) {
		if (formulaExist(conclusion)) return;
		InferenceHistoryNode node = new InferenceHistoryNode(assumptions, usedAxiom, conclusion);
		this.history.addHistory(conclusion, node);
	}
	
	public Set<RDLTerm> getExistTerms() {
		Set<RDLTerm> result = new HashSet<>();
		result.addAll(dependencies);
		result.addAll(evaluatableTerms);
		return result;
	}
	
	public boolean formulaExist(Formula formula) {
		if (formula instanceof EquationFormula eq) {
			return this.equationFormulas.contains(eq);
		} else if (formula instanceof DependencyFormula df) {
			return this.dependencyFormulas.contains(df);
		}
		return false;
	}
	
	record ConclusionMatchedTerm(Set<EvaluatableTerm> leftSideHands, Set<EvaluatableTerm> rightSideHands) {};
	
}