package inference.equivalence;

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import models.algebra.Constant;
import models.algebra.Term;
import models.algebra.Variable;
import models.dataConstraintModel.DataConstraintModel;
import models.terms.LinearRightNormalizedType;
import models.terms.RDLTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResourceVariable;

public class SemanticEquivalenceProofSystem {

	private Map<Integer, List<SemanticEquivalenceRelation>> assumptions;
	private SemanticEquivalenceRelation conclusion;
	int maxOrder = -1;
	
	private static MetaSemanticEquivalenceRelation rule1 = new MetaSemanticEquivalenceRelation(
			new MetaRDLTerm(
					new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))),
					new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))),
					new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED)
			),
			new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED),
			new Variable("n")
	);
	
	private static MetaSemanticEquivalenceRelation rule4_1 = new MetaSemanticEquivalenceRelation(
			new MetaEvaluatableTermVariable(new Variable("t"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED),
			new MetaEvaluatableTermVariable(new Variable("t'"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED),
			new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))
	);
	
	public SemanticEquivalenceProofSystem(Collection<SemanticEquivalenceRelation> assumptions, SemanticEquivalenceRelation conclusion) {
		for(SemanticEquivalenceRelation assumption : assumptions) {
			maxOrder = Math.max(maxOrder, assumption.getOrder());
			if (! this.assumptions.containsKey(assumption.getOrder())) {
				this.assumptions.put(assumption.getOrder(), new ArrayList<>());
			}
		}
		this.conclusion = conclusion;
	}
	
	public boolean proof() {
		Set<RDLTerm> existTerms = new HashSet<>();
		for(int key : assumptions.keySet()) {
			for(SemanticEquivalenceRelation relation : assumptions.get(key)) {
				existTerms.addAll(relation.getLeftSideHand().getSubTerms(RDLTerm.class).values());
				existTerms.add(relation.getLeftSideHand());
				existTerms.addAll(relation.getRightSideHand().getSubTerms(RDLTerm.class).values());
				existTerms.add(relation.getRightSideHand());
			}
		}
		for (int i = maxOrder; i > 0; i--) {
			
		}
		return false;
	}
	
}